Nuprl Lemma : comb_for_pi2_wf
2,24
postcript
pdf
(
A
,
B
,
p
,
z
. 2of(
p
))
A
:Type
B
:(
A
Type)
p
:
a
:
A
B
(
a
)
True
B
(1of(
p
))
latex
Definitions
T
,
x
:
A
.
B
(
x
)
,
t
T
,
True
,
x
(
s
)
Lemmas
true
wf
,
squash
wf
,
pi2
wf
origin
A,B,p,z. 2of(p)) 
A:Type
B:(AType)p:a:A
B(a)
TrueB(1of(p)) A,B,p,z. 2of(p)) A:TypeB:(AType)p:a:AB(a)TrueB(1of(p)) T
x:A. B(x) T